
Lemma everything_is_itself:
    forall x: Set, x = x.
Proof.
    intros.
    reflexivity.
Qed.